| Definitions | sys-antecedent(es;Sys), x:A  B(x),  x:A. B(x), t  T, s = t, P   Q, chain-consistent(f;chain), ES, Type, AbsInterface(A),  , <a, b>,  , E, type List, x:A  B(x),  b, left + right, {x:A| B(x)} , Top, E(X), f(a), Id, y is f*(x), x << y, x <<= y,  A, P & Q,  x:A. B(x), let x,y = A in B(x;y), t.1, a:A fp B(a), strong-subtype(A;B), e c e', EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), EState(T), Knd,   x. t(x), x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M),  ,  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r s, constant_function(f;A;B), e  X, loc(e), kind(e), SWellFounded(R(x;y)), pred!(e;e'), !Void(),  x:A.B(x), S  T, suptype(S; T), first(e), pred(e), x.A(x), loc(e), X(e), P  Q, a < b, hd(l), L1 L2, e loc e' , adjacent(T;L;x;y), (x l), no_repeats(T;l), f**(e), False, y=f*(x) via L, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , x before y l, {T}, kind(e), first(e), (e <loc e'), s ~ t, SQType(T), source(l), destination(l), es-init(es;e), P  Q, P Q, Atom$n, isrcv(e), es-first-from(es;e;l;tg), isrcv(k), lastchange(x;e), (last change to x before e), last(L), True,  T, A c B, {i..j }, x dom(f), a = b, locl(a), Dec(P), l_disjoint(T;l1;l2), MaName, (e < e'), e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e),  , A B, Atom, x,y:A//B(x;y), b | a, a ~ b, |p|, a b, a <p b, |g|, a < b, x f y, |r|, xL. P(x), (xL.P(x)),  , r < s, q-rel(r;x), Outcome, dstype(TypeNames; d; a), ff, inr x , tt, inl x , SqStable(P), a =!x:T. Q(x), InvFuns(A;B;f;g), Inj(A;B;f), IsEqFun(T;eq), Refl(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Trans(T;x,y.E(x;y)), AntiSym(T;x,y.R(x;y)), Connex(T;x,y.R(x;y)), CoPrime(a,b), Ident(T;op;id), Assoc(T;op), Comm(T;op), Inverse(T;op;id;inv), BiLinear(T;pl;tm), IsBilinear(A;B;C;+a;+b;+c;f), IsAction(A;x;e;S;f), Dist1op2opLR(A;1op;2op), fun_thru_1op(A;B;opa;opb;f), FunThru2op(A;B;opa;opb;f), Cancel(T;S;op), monot(T;x,y.R(x;y);f), IsMonoid(T;op;id), IsGroup(T;op;id;inv), IsMonHom{M1,M2}(f), a b, IsIntegDom(r), IsPrimeIdeal(R;P), f g, f(x)?z, ||as||, n+m, -n, n - m, i j < k, #$n, l[i], b, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, deq-member(eq;x;L), e = e', p q, p q, p q, increasing(f;k), [], [car / cdr], A List |
| Lemmas | chain-pullback, es-interface-subtype rel, fun-connected transitivity, before-adjacent, l tricotomy, l member wf, chain-consistent-member, adjacent-member, member sublist, hd-before, l member subtype, chain-order-antisymmetric, increasing wf, length wf nat, le wf, bool cases, eqtt to assert, bool sq, iff transitivity, eqff to assert, assert of bnot, bnot wf, int seg wf, length wf1, select wf, adjacent wf, sq stable from decidable, decidable assert, btrue wf, bfalse wf, fun-connected-step, decidable wf, decidable equal Id, chain-order transitivity, chain-order-antireflexive, fun-connected-induction, all functionality wrt iff, implies functionality wrt iff, exists functionality wrt iff, and functionality wrt iff, assert-eq-id, eq id wf, es-first wf, es-interface-val wf2, l before wf, fun-path wf, fun-connected weakening eq, true wf, squash wf, iff wf, rev implies wf, es-isrcv-loc, Id sq, es-le-loc, es-le wf, es-loc-pred, false wf, guard wf, es-loc wf, kind wf, loc wf, first wf, pred! wf, strongwellfounded wf, es-is-interface wf, es-causle wf, es-interface wf, top wf, constant function wf, bool wf, qle wf, cless wf, val-axiom wf, rationals wf, nat wf, Msg wf, kindcase wf, Knd wf, EState wf, EOrderAxioms wf, IdLnk wf, unit wf, deq wf, event system wf, sys-antecedent wf, es-E-interface-subtype rel, member wf, es-E wf, subtype rel wf, not wf, Id wf, chain-order-le wf, chain-order wf, assert wf, fun-connected wf, es-E-interface wf, chain-consistent wf |
